\begin{tabbing}
ES(${\it the\_w}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\langle$E\+
\\[0ex]$,\,$product{-}deq(Id;$\mathbb{N}$;IdDeq;NatDeq)
\\[0ex]$,\,$($\lambda$$e$.w{-}pred(${\it the\_w}$;$e$))
\\[0ex]$,\,$($\lambda$$e$.w{-}info(${\it the\_w}$;$e$))
\\[0ex]$,\,$(TERMOF\{w{-}order{-}axioms:ObjectId, 1:l, i:l\}(${\it the\_w}$,$p$))
\\[0ex]$,\,$${\it the\_w}$.T
\\[0ex]$,\,$${\it the\_w}$.TA
\\[0ex]$,\,$${\it the\_w}$.M
\\[0ex]$,\,$($\lambda$$i$,$x$. s($i$;0).$x$)
\\[0ex]$,\,$($\lambda$$i$.1of(2of(w{-}machine(${\it the\_w}$;$i$))))
\\[0ex]$,\,$($\lambda$$e$.val($e$))
\\[0ex]$,\,$($\lambda$$i$.2of(2of(w{-}machine(${\it the\_w}$;$i$))))
\\[0ex]$,\,$($\lambda$$i$.1of(w{-}machine(${\it the\_w}$;$i$)))
\\[0ex]$,\,$(TERMOF\{world{-}es{-}val:ObjectId, 1:l, i:l\}(${\it the\_w}$,$p$))
\\[0ex]$,\,$(TERMOF\{world{-}es{-}atom:ObjectId, 1:l, i:l\}(${\it the\_w}$,$p$))
\\[0ex]$,\,$$\cdot$$\rangle$
\-
\end{tabbing}